A:Type, d:EqDecider(A), i:A. sqequal((eqof(d)(i,i)); tt) 

latex

Definitions	x:A. B(x), eqof(d), t  T, t.1, P  Q, prop{i:l}, EqDecider(T), sq_type(T), guard(T), , P  Q, P  Q, Unit, A, False, tt, , ff
Lemmas	bool sq, deq wf, bool wf, eqtt to assert, btrue wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot